(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
monus(S(x'), S(x)) → monus(x', x)
gcd(x, y) → gcd[Ite](equal0(x, y), x, y)
equal0(a, b) → equal0[Ite](<(a, b), a, b)
The (relative) TRS S consists of the following rules:
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
gcd[Ite](False, x, y) → gcd[False][Ite](<(x, y), x, y)
gcd[Ite](True, x, y) → x
gcd[False][Ite](False, x, y) → gcd(y, monus(y, x))
gcd[False][Ite](True, x, y) → gcd(monus(x, y), y)
equal0[Ite](False, a, b) → False
equal0[Ite](True, a, b) → equal0[True][Ite](<(b, a), a, b)
equal0[True][Ite](False, a, b) → False
equal0[True][Ite](True, a, b) → True
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
monus(S(x'), S(x)) →+ monus(x', x)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [x' / S(x'), x / S(x)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)